Library ConwayPermutations

Require Export ConwayNotations.
Require Export PointsType.
Require Import Fourier.

Section Triangle.

Context `{M:triangle_theory}.

Variable ineq_1 : a + b - c >0.
Variable ineq_2 : a - b + c >0.
Variable ineq_3 : -a + b + c >0.

Lemma delta_ok :
 0 ≤ (a + b - c) × (a - b + c) × (- a + b + c) × (a + b + c).
Proof.
apply Rmult_le_pos.
apply Rmult_le_pos.
apply Rmult_le_pos.
fourier.
fourier.
fourier.
fourier.
Qed.

Lemma sqrt_square : ∀ x, 0≤x → (sqrt x)^2 = x.
Proof.
intros.
simpl.
replace (sqrt x × 1) with (sqrt x) by ring.
apply sqrt_sqrt.
assumption.
Qed.

Lemma Delta_square_util : DeltaMaj a b c × (DeltaMaj a b c × 1) = 1/16*(((a+b-c)*(a-b+c)*(-a+b+c)*(a+b+c))).
Proof.
unfold DeltaMaj.
ring_simplify.
rewrite sqrt_square .
field.
apply delta_ok.
Qed.

Lemma Delta_perm_1 : DeltaMaj a b c = DeltaMaj b c a.
Proof.
unfold DeltaMaj.
f_equal. f_equal.
ring.
Qed.

Lemma Delta_perm_2: DeltaMaj a b c = DeltaMaj c a b.
Proof.
unfold DeltaMaj.
f_equal. f_equal.
ring.
Qed.

Lemma SS_perm_1: SS a b c = SS b c a.
Proof.
unfold SS.
f_equal.
unfold DeltaMaj.
f_equal.
f_equal.
ring.
Qed.

Lemma SS_perm_2: SS a b c = SS c a b.
Proof.
unfold SS.
f_equal.
unfold DeltaMaj.
f_equal.
f_equal.
ring.
Qed.

Lemma J_perm_1: J a b c = J b c a.
Proof.
unfold J.
f_equal. f_equal.
ring.
ring.
Qed.

Lemma J_perm_2: J a b c = J c a b.
Proof.
unfold J.
f_equal. f_equal.
ring.
ring.
Qed.

Lemma e_perm_1: e a b c = e b c a.
Proof.
unfold e.
f_equal. f_equal.
ring.
ring.
Qed.

Lemma e_perm_2: e a b c = e c a b.
Proof.
unfold e.
f_equal. f_equal.
ring.
ring.
Qed.

Lemma RR_perm_1: RR a b c = RR b c a.
Proof.
unfold RR.
f_equal.
ring.
f_equal.
ring.
Qed.

Lemma RR_perm_2: RR a b c = RR c a b.
Proof.
unfold RR.
f_equal.
ring.
f_equal.
ring.
Qed.

Lemma r_perm_1: r a b c = r b c a.
Proof.
unfold r.
f_equal.
f_equal.
f_equal.
ring.
ring.
Qed.

Lemma r_perm_2: r a b c = r c a b.
Proof.
unfold r.
f_equal.
f_equal.
f_equal.
ring.
ring.
Qed.

End Triangle.